(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Bool)
(declare-fun m () Real)
(declare-fun n () Bool)
(declare-fun o () Bool)
(declare-fun p () Bool)
(assert (= (+ (* (ite e 1 0))) (+ (+ (+ (* (ite p 1 0) (ite o 1 0) (ite b 1 0) (ite a 1 0) (ite d 1 0) (ite c 1 0) (ite g 1 0) (ite f 1 0)))) (ite i 1 0) (ite h 1 0)) (* 2.0 (+ (ite k 1.0 0.0))) (+ (ite j 1.0 0.0) (ite l 1.0 0.0) (ite n 1.0 0.0))))
(check-sat)
